activation chain
Confluence of Reduction Rules for Lexicographic Ordering Constraints
Grayland, Andrew (University of St. Andrews) | Miguel, Ian (University of St. Andrews) | Roney-Dougal, Colva M. (University of St. Andrews)
The lex leader method for breaking symmetry in CSPs typically produces a large set of lexicographic ordering constraints. Several rules have been proposed to reduce such sets whilst preserving logical equivalence. These reduction rules are not generally confuent: they may reach more than one xpoint, depending on the order of application. These fixpoints vary in size. Smaller sets of lex constraints are desirable so ensuring reduction to a global minimum is essential. We characterise the systems of constraints for which the reduction rules are confluent in terms of a simple feature of the input, and define an algorithm to determine whether a set of lex constraints reduce confuently.